A:Type, eq:EqDecider(A), B:(AType), f:fpf(A; a.B(a)), x:A, v:B(x).
((fpf-dom(eq; x; f)))  fpf-compatible(A; a.B(a); eq; f; fpf-single(x; v)) 

latex

Definitions	t  T, x(s), x:A. B(x), x. t(x), top, fpf(A; a.B(a)), fpf-dom(eq; x; f), b, False, P  Q, A, P  Q, P  Q, fpf-single(x; v), prop{i:l}, fpf-ap(f; eq; x), fpf-compatible(A; a.B(a); eq; f; g), EqDecider(T)
Lemmas	not wf, fpf wf, deq wf, fpf-single wf, top wf, fpf-single-dom, assert wf, fpf-dom wf, fpf-trivial-subtype-top